% !Mode:: "TeX:UTF-8"
\head{Алгебраическая модель}
Это набор аксиом вида равенства термов. Пример:
\begin{lstlisting}
scheme Addition = class
        value add: Int >< Int -> Int
        axiom forall x, y, z: Int :-
            add(add(x,y),z) is add(x, add(y, z)),
            add(x,y) is add(y,x),
            add(x,0) is x
end
\end{lstlisting}

Алгебраические модели тесно связаны с понятием \emph{абстрактных типов данных} (АТД). Собственно, алгебраические модели являются одним из способов задания АТД. Например, <<стек --- это нечто, удовлетворяющее принципу LIFO>>:
\begin{lstlisting}
type Stack, Elem
value push: Stack >< Elem -> Stack,
      pop: Stack -~-> Elem >< Stack
axiom forall s: Stack, e: Elem :-
      pop( push(s,e) ) is (e, s)
\end{lstlisting}

Идея алгебраического моделирования состоит в разделении системы на набор компонентов (похожим образом в рамках объектно-ориентированного анализа выделяются классы анализа), каждый компонент воспринимается как АТД: для них определяется функциональный интерфейс и строятся алгебраические аксиомы.

Важно также понимать, что хотя состояние компонента при этом явно не моделируется, думать о нем всё равно нужно и составлять алгебраическую модель надо, исходя из представления о состоянии.

Пример алгебраического моделирования списка (L --- список, упорядоченная последовательность, элементов типа E):
\begin{lstlisting}[escapechar={|}]
type E, L
value empty: L,
      add: L >< E -> L,
      |is\_in|: L >< E -> Bool
axiom forall l: L, e,e1: E :-
  ~|is\_in|(empty, e),
  |is\_in|(add(l,e), e1) is e = e1 \/ |is\_in|(l,e1)
\end{lstlisting}

Однако ровно те же аксиомы выполнены, и если L --- это множество элементов типа E ! Разные коллекции элементов -- а спецификации одинаковые? Где ошибка? Ошибка в том, что в действительности описан не список, а нечто более абстрактное: некое хранилище элементов, где не один элемент не пропадает. И множество, и список являются таким хранилищем. Но они обладают дополнительными требованиями, которые не выражены в этой спецификации.

\head{Области действия, аксиомы с предусловиями}

Важно понимать \emph{область действия} аксиомы. Под такой областью будем понимать значения переменных, находящихся в самом внешнем кванторе всеобщности. Например, в последнем примере это все возможные стеки s и добавляемые элементы e. Но не во всех случаях допустимо использовать все допустимые типом значения. Например, следующая спецификация неверно описывает очередь:
\begin{lstlisting}
type Queue, Elem
value empty: Queue,
      add: Queue >< Elem -> Queue,
      first: Queue -~-> Elem
axiom forall q: Queue, e: Elem :-
      first( add(q,e) ) is e
\end{lstlisting}

Она справедлива, только если q = empty. Для ограничения области действия нужно использовать \textbf{pre}-выражения:
\begin{lstlisting}
axiom forall q: Queue, e: Elem :-
      first( add(q,e) ) is e  pre q = empty
\end{lstlisting}

На самом деле последнюю аксиому можно записать короче:
\begin{lstlisting}
axiom forall e: Elem :-
      first( add(empty,e) ) is e
\end{lstlisting}

Предусловие обязательно для тех термов, которые определены не для всех значений переменных, находящихся под внешним квантором всеобщности.

\head{Обсерверы, генераторы}

Даже если для специфицируемого компонента не моделируется состояние, это не означает, что его нет. Оно есть. Это значит, что есть и операции, которые переводят компонент из одного состояния в другой. Будем называть такие операции \emph{генераторами}. Но поскольку идея property-based моделирования в описания эффекта, который осуществляют операции, нужны способы описания состояний. Воспользуемся атрибутным описанием: для состояния будем определять его описывающие атрибуты. Такие операции-атрибуты будем называть \emph{обсерверами} (их аналогами в языке Java и некоторых других объектно-ориентированных языках программирования являются методы-getter'ы).

В алгебраической спецификации программного компонента обязательно будет присутствовать тип для состояния компонента --- \emph{целевой тип}. В операции-обсервере одним из аргументов должен быть целевой тип. В операции-генераторе один из возвращаемых значений должен быть целевого типа. Пример:
\begin{lstlisting}[escapeinside=`']
type Queue, - - - `целевой тип'
     Elem - - - `это не целевой тип'
value add: Queue >< Elem -> Queue, - - - `генератор'
      first: Queue -~-> Elem - - - `обсервер'
\end{lstlisting}

% что делать с функциями, у которых два целевых типа на входе?

% что делать с функциями, у которых два целевых типа на выходе? --- их можно разделить на две функции

\head{Термы и их значения}

Не стоит забывать, что терм, цепочка вызовов функций, есть всего лишь набор символов, за которым изначально не закреплено никакого значения. Наоборот --- аксиомы обозначают классы эквивалентности цепочек: эквивалентные цепочки имеют одинаковые значения, неэквивалентные --- различные. При этом эквивалентные цепочки могут иметь совершенно различную длину, могут состоять из различных функций. Если не сказано явно, при написании и чтении алгебраических спецификаций \textbf{нельзя} принимать очевидные соображения за действительные в отношении цепочек функций. Например, из такой спецификации
\begin{lstlisting}
type E, S
value empty: S,
      add: S >< E -> S
\end{lstlisting}
совершенно не следует, что add всегда будет давать значения, отличные от empty. Равно как и не следует, что add будет давать различные значения на различных аргументах и длинах цепочек вызовов add (см. соответствующую задачу). Т.е. любой генератор может игнорировать свои аргументы, использовать их в таком виде, как они переданы, или сначала модифицировать, а затем воспользоваться ими.

Но всё же известные свойства генераторов надо показывать в спецификации. Для этого есть 3 способа:
\begin{enumerate}
  \item использовать вариантные определения; например, такая запись
      \begin{lstlisting}
        type E, S == empty | add(S,E)
      \end{lstlisting}
      включает в себя не только сигнатуры empty и add, но и аксиому о том, что add(s,e) $\Not$= empty для любых s и e соответствующих типов;

  \item использовать аксиомы на термы из генераторов; например, такая запись скажет, что в хранилище нет повторных элементов:
\begin{lstlisting}
type E, S
value empty: S,
      add: S >< E -> S
axiom forall s:S, e, e1, e2: E :-
    add(add(s,e),e) is add(s,e),
    add(add(s,e1),e2) is add(add(s,e2),e1)
\end{lstlisting}
     Другой пример аксиом на термы из генераторов --- это наличие <<обратных>> генераторов:
\begin{lstlisting}
type E, L == empty | add(L,E)
value point: L -> Nat,
    size: L -> Nat,
    next: L -~-> L,
    prev: L -> L
axiom forall l: L :-
     prev( next( l ) ) is l pre point(l) < size(l),

     point(next(l)) is point(l)+1 pre point(l)<size(l),
     next(l) is l pre point(l) = size(l),
     point(prev(l)) is point(l) - 1 pre point(l) > 0,
     prev(l) is l pre point(l) = 0,
\end{lstlisting}
Или более классический пример --- про бесконечный стек:
\begin{lstlisting}
type E, L == empty | push(L,E)
value pop: L -~-> L
axiom forall l: L, e: E :-
     pop( push(l, e) ) is l
\end{lstlisting}
%Предыдущий пример то же в виде аксиомы над обсерверами:
%\begin{lstlisting}
%type E, L == empty | add(L,E)
%value next: L >< E -~-> E,
%        prev: L >< E -~-> E
%axiom forall l: L, e: E :-
%     prev( l, next(l, e) ) is e
%\end{lstlisting}

   \item использовать дополнительные обсерверы с тотальными определениями; если такие обсерверы дадут при двух вызовах разные результаты, то аргументы этих обсерверов разные; например, в этой спецификации
\begin{lstlisting}
type E, S
value empty: S,
      add: S >< E -> S
value check: S >< E -> Bool
axiom forall s:S, e, e1: E :-
    ~check(empty, e),
    check(add(s,e),e1) is e = e1 \/ check(s,e1)
\end{lstlisting}
    check(empty, e) is false и check(add(empty,e),e) is true, значит, из этой спецификации следует, что empty $\Not$= add(empty,e).
\end{enumerate}

Последний пример можно расширить следующим образом: для любой функции $f$ с тотальным определением выполнено следующее свойство <<для любых ее (допустимых своими типами) аргументов $x$ и $y$ выполнено, что $x \Is y ~\Implies~\\ f(x) \Is f(y)$>>. Из этого свойства \textbf{для функций с тотальным определением} $f$ справедливо следующее: $f(x) \Neq f(y) ~\Implies~ x \Neq y$. Если в качестве $f$ рассматривать один из обсерверов (или генераторов) и возможно составить две цепочки $f(x)$ и $f(y)$, про которые доподлинно известно, что их значения различны, то можно утверждать, что значения и $x$ с $y$ различные. В такой форме это свойство бывает крайне полезно для того, чтобы понять, какие термы должны иметь различные значения. Грубо говоря, если обсервер должен выделять некие данные из состояния (<<должен>> --- т.к. он тотальный), то генератор должен эти данные поместить и не игнорировать, в результате чего получаются разные состояния из-за разных вложенных туда данных.

Важный и не всегда очевидный момент: аксиомы алгебраической спецификации определяют не только функциональность операций (в первую очередь, обсерверов), но и свойства состояния, практически его структуру (но явно эта структура, конечно же, не задается).

И, конечно, не стоит забывать, что термы и функции в языках спецификации --- это лишь математические абстракции. Они не размещены в какой-либо <<памяти>>, нет способа адресации к ним, нет указателей, нет ссылок на структуры, нет понятия динамической памяти, нет понятия времени исполнения функции --- все функции <<мгновенно>> строят возвращаемое значение по входным параметрам.

\head{Конфлюэнтность, нормальные формы термов}

Хотя специфицируются абстрактные типы данных, множество значений этих типов всё же можно выразить при помощи классов эквивалентности термов (каждому классу будет соответствовать своё значение АТД). Например, для базы данных значение может быть задано термом add(<<Иванов>>, 200, add(<<Петров>>, 500, empty)). Терм соответствует некоторому состоянию моделируемой системы. Известен факт о том, что нельзя написать алгоритм, который бы по любой алгебраической спецификации и двум данным термам определял, эквивалентны эти термы или нет\footnote{Взяв первый терм, пытаемся вставить его на место аргументов в аксиомах и сделать подстановку левой части аксиомы на правую. Так получаем новый терм. К нему применяем то же правило --- получаем еще один терм. Если в результате таких преобразований когда-нибудь получился второй терм, значит первый и второй термы эквивалентны, они означают одинаковые состояния моделируемых систем. А если второй терм никогда не будет получен, то первый и второй термы неэквивалентны. Получается <<алгоритм>>, который должен зацикливаться. Естественно, это означает отсутствие алгоритма в правильном понимании этого слова.}. Из-за этого, проанализировав систему на ряде цепочек, невозможно (для произвольной алгебраической спецификации) понять, во всех ли состояниях система проанализирована.

Хороши те системы аксиом, которые дают \emph{нормальные формы} термов. Системы с такими аксиомами проще анализировать и проще понимать их смысл, поскольку есть понятная классификация состояний-термов. Например, для списка состоянием является последовательность элементов $\langle x_1, x_2, ..., x_n \rangle$ --- очевидно алгебраическое представление списка, являющееся нормальной формой: \texttt{cons($x_1$, cons($x_2$, ..., cons($x_n$, nil) ... ))}; В случае нормальной формы можно даже сформулировать условия достаточности: для полного анализа достаточно исследовать все свойства только на термах, являющихся нормальными формами.

Итог: при выделении операций-генераторов надо постараться так, чтобы каждое значение целевого типа имело единственной представление в виде терма из этих операций (т.н. \emph{нормальная форма}). В том числе может быть придется добавить дополнительные аксиомы, чтобы было возможно при помощи них доказательно отождествить разные термы.

Но и выделив нормальную форму, при написании аксиом нельзя забывать о существовании термов, не находящихся в нормальной форме: для них аксиома тоже должна быть справедлива (а при анализе системы про такие термы забыть можно). Пример: множество -- не забыть аксиому add(a, add(b,c)) is add(b, add(a,c))   (нормальная форма: add(add(add с возрастающими аргументами, в том числе без повторов). Например, правильной аксиомой для delete(add) будет для множеств такая: delete(x, add(y,s)) is if x = y then delete(x,s) else add(y, delete(x,s)) end (т.е. в then ветви не просто s, а delete(x,s) -- вдруг x встретится \textbf{в терме} еще раз).

